(declare-fun a () String)
(declare-fun b () String)
(declare-fun c () String)
(declare-fun d () String)
(declare-fun e () Int)
(declare-fun f () String)
(declare-fun T4_6 () String)
(declare-fun g () Bool)
(declare-fun h () Bool)
(declare-fun i () String)
(assert (ite g (and (distinct e 0) (distinct (str.substr a 6 0) (str.++ (str.substr b 4 (str.len f)))) (not (str.in_re (str.substr d 8 (str.len T4_6)) (re.++ (str.to_re "_") (re.++ (str.to_re "_") (re.++ (str.to_re "u") (re.++ (str.to_re "t") (re.++ (str.to_re "m") (re.++ (str.to_re "a") (re.union (str.to_re "=") (re.++ (re.++ (str.to_re "6") (re.++ (str.to_re "8") (re.++ (str.to_re "8"))))))))))))))) (not (str.in_re (str.substr a 6 0) (re.++ (str.to_re "u") (str.to_re "m"))))))
(assert (distinct h (= (str.substr b (str.len f) (str.len (str.substr c 0 (str.len (str.substr d 0 (str.len i)))))) "")))
(assert h)
(assert (= b (str.++ f i)))
(assert (distinct d (str.++ T4_6 i)))
(check-sat)
(assert (ite g (and (distinct e 0) (distinct (str.substr a 6 0) (str.++ (str.substr b 4 (str.len f)))) (not (str.in_re (str.substr d 8 (str.len T4_6)) (re.++ (str.to_re "_") (re.++ (str.to_re "_") (re.++ (str.to_re "u") (re.++ (str.to_re "t") (re.++ (str.to_re "m") (re.++ (str.to_re "a") (re.union (str.to_re "=") (re.++ (re.++ (str.to_re "6") (re.++ (str.to_re "8") (re.++ (str.to_re "8"))))))))))))))) (not (str.in_re (str.substr a 6 0) (re.++ (str.to_re "u") (str.to_re "m"))))))
(assert (distinct h (= (str.substr b (str.len f) (str.len (str.substr c 0 (str.len (str.substr d 0 (str.len i)))))) "")))
(assert h)
(assert (= b (str.++ f i)))
(assert (distinct d (str.++ T4_6 i)))
(check-sat)
